T:Type, z:T List. ||z|| = 2    z = [z[0]; z[1]] 

latex

Definitions	t  T, P  Q, x:A. B(x), ij, ||as||, False, A, AB, , Prop, l[i], hd(l), i<j, ij, tl(l)
Lemmas	nat wf, length wf2, select wf, length wf1, non neg length